Nuprl Definition : p-open-member
11,40
postcript
pdf
s
C
==
n
:
. (
C
(<
n
,
s
>) = 1)
latex
clarification:
p-open-member(
p
;
C
;
s
) ==
n
:
. (
C
(<
n
,
s
>) = 1
)
latex
Definitions
x
:
A
.
B
(
x
)
,
,
s
=
t
,
,
f
(
a
)
,
<
a
,
b
>
,
#$n
FDL editor aliases
p-open-member
origin
C == 
n:
. (C(<n, s>) = 1)
n:. (C(<n, s>) = 1 
) C == n:. (C(<n, s>) = 1)
n:. (C(<n, s>) = 1 ) x:A. B(x)